Идея для дисера, дарю!

Рабочее название: Непрерывные отображения лямбда термов

Вот вам идея для комбинаторной задачи. Сортируем, т.е. создаем порядок, или
набор перестановок всех возможных пар типовых сигнатур, расстояние между
которыми не больше чем добавление/удаление одной лямбды или квантора из
сигнатурной цепочки (индуктивные типы aka полиномиальные функторы просто
кодируются длинными цепочками).

Пример. Точка — Юнит. Две точки — Булевый тип. Две точки и одна перменная —
например обработчик ошибок OK | Err reason. Две точки и две переменных —
протокол с кодом возврата OK value | Err reason. Или другое ветвление. Две
точки, одна переменная и рекурсивное зацикливание или петля — List A = Nil |
Cons A (List A). И так далее. Если вы запустите генератор такой группы (какая у
нее симметрия?) то вы получите все возможные базовые библиотеки функциональных
языков программирования. Напоминаю, согласно МакБрайду орнамента всего три:
точка, переменная и рекурсивное зацикливание. Ну и переменных может быть любое
количество, кодировать нумералами черча, как и вселенные.

В гомотопической теории еще конструктор Пути, или просто говоря равенство,
четвертый орнамент. Там альтернативное ветвление такое. Путь — Отрезок. Точка и
Путь — S1. Но конструктор пути многомерный! Поэтому. Сфера — это Точка и
двумерный путь (движение одномерного пути). Дальше высшие сферы, конусы,
надстройки и так далее. Возможно добавление трех предыдущих орнаментов, что
означает добавление носителя, т.е. для первых поллов генератора — типы
натуральных Nat = 0 | S Nat, целых Z = 0 | S | P, действительных R = Stream
Digit чисел. Да, да, для действительных чисел нужна корекурсия и коиндуктивные
типы, простейший из которых стрим. Стрим от листового конса отличается тем что
у него элиминатор и интродакшин поменяны местами.

Добавление генерации коиндуктивных сигнатур будет создавать все возможные
конкурентные программы изоморфные акторам и прочим моделям, которых множество,
включая сети петри и прочую лабуду. Это врата в пи калкулус, линейные типы и
другие категории. Пи калкулус — это когда мы паралельно можем симулировать
выбранные нами коиндуктивные стримы. Все распределенные алгоритмы работают в
этих категориях.

Кто нарисует карту? Так что б до монад хотябы. Можно будет создать роботов,
которые будут искать неведанные нам сигнатуры и пытаться доказывать неведанные
теоремы или находить точки в этих высших пространствах. Естественно все это
подключить к роботам из бостон дайнамикс, или что там вселяет ужас в гуманоидов.